$\forall$$i$,$a$:Id, $p$:finite{-}prob{-}space, ${\it ds}$:fpf(Id; $x$.Type), $P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex]normal{-}ds\{i:l\}(${\it ds}$) $\Rightarrow$ R{-}realizes\{i:l\}(Rpre($i$; ${\it ds}$; $a$; $p$; $P$); ${\it es}$.pre{-}p(${\it es}$; $i$; ${\it ds}$; $a$; $p$; $P$))